#include "PDTGraphVisitor.h"
#include "PDTNode.h"
#include "PDTNumVar.h"
#include "PDTNumConst.h"
#include "PDTBoolVar.h"
#include "PDTBoolConst.h"
#include "PDTFunction.h"
#include "PDTProp.h"

extern "C"{
yicesl_context yices_get_lite_context(yices_context);
}
/*
DefaultVistor traverses the code structure and outputs it in text form.
*/

/*
  pre is executed before traversing the children
*/
bool PDTDefaultVisitor::pre(PDTNode * me){
	NodeTypeEnum type =me->getType();

	switch (type)
	{
	case PDTNumVar_Em:
		cout<<((PDTNumVar *)me)->getName();
		break;
	case PDTNumConstInt_Em:
		cout<<((PDTNumConstInt *)me)->getValue();
		break;
	case PDTNumConstDbl_Em:
		cout<<((PDTNumConstDbl *)me)->getValue();
		break;
	case PDTBoolVar_Em:
		cout<<((PDTBoolVar *)me)->getName();
		break;
	case PDTBoolConst_Em:
		cout<<((PDTBoolConst *)me)->getValue();
		break;
	case PDTAdd_Em:
		cout<<"(";
		break;
	case PDTSubt_Em:
		cout<<"(";
		break;
	case PDTMult_Em:
		cout<<"(";
		break;
	case PDTDiv_Em:
		cout<<"(";
		break;
	case PDTMod_Em:
		cout<<"(";
		break;

	case PDTAssign_Em:
		;
		break;
	case PDTWhile_Em:
		cout<<"while( ";
		break;
	case PDTFunctionDec_Em:
		cout<<((PDTFunctionDec*)me)->name<<" (";
		break;
	case PDTIfElse_Em:
		cout<<"if( ";
		break;
	case PDTAnd_Em:
		cout<<"(";
		break;
	case PDTOr_Em:
		cout<<"(";
		break;
	case PDTLessThan_Em:
		cout<<"(";
		break;
	case PDTGreaterThan_Em:
		cout<<"(";
		break;
	case PDTLessThanEqual_Em:
		cout<<"(";
		break;
	case PDTGreaterThanEqual_Em:
		cout<<"(";
		break;
	case PDTEqualNum_Em:
		cout<<"(";
		break;
	case PDTEqualBool_Em:
		cout<<"(";
		break;
	case PDTNotEqualNum_Em:
		cout<<"(";
		break;
	case PDTNotEqualBool_Em:
		cout<<"(";
		break;
	case PDTNeg_Em:
		cout<<"-";
		break;
	case PDTNot_Em:
		cout<<"!";
		break;
	case PDTListOfStatements_Em:
		;
		break;
	default:
		;
	}
	return true;
}
/*
  in is executed between two children traversals (starts after the first child and ends after the last child)
*/
bool PDTDefaultVisitor::in(PDTNode * me, PDTNode* child, unsigned int i){
	NodeTypeEnum type =me->getType();
	//NodeTypeEnum childType=child->getType();
	switch (type)
	{
/*	case (PDTNumVar_Em||PDTNumConstInt_Em||PDTNumConstDbl_Em||PDTBoolVar_Em||PDTBoolConst_Em):
		break;
*/
	case PDTAdd_Em:
		if (i==0)
			cout<<"+";
		break;
	case PDTSubt_Em:
		if (i==0)
			cout<<"-";
		break;
	case PDTMult_Em:
		if (i==0)
			cout<<"*";
		break;
	case PDTDiv_Em:
		if (i==0)
			cout<<"/";
		break;
	case PDTMod_Em:
		if (i==0)
			cout<<"%";
		break;
	case PDTAssign_Em:
		if (i==0)
			cout<<"=";
		break;
	case PDTWhile_Em:
		if (i==0)
			cout<<") {\n";
		break;
	case PDTFunctionDec_Em:
		if (i<((PDTFunctionDec*)me)->children.size()-3)
			cout<<" ";
		else if (i==(((PDTFunctionDec*)me)->children.size()-3))
			cout<<") {\n ";
		else if (i==(((PDTFunctionDec*)me)->children.size()-2))
			cout<<"return ";
		break;
	case PDTIfElse_Em:
		if (i==0)
			cout<<") {\n";
		else if (i==1)
			cout<<"}\nelse {\n";
		break;
	case PDTAnd_Em:
		if (i==0)
			cout<<"&&";
		break;
	case PDTOr_Em:
		if (i==0)
			cout<<"||";
		break;
	case PDTLessThan_Em:
		if (i==0)
			cout<<"<";
		break;
	case PDTGreaterThan_Em:
		if (i==0)
			cout<<">";
		break;
	case PDTLessThanEqual_Em:
		if (i==0)
			cout<<"<=";
		break;
	case PDTGreaterThanEqual_Em:
		if (i==0)
			cout<<">=";
		break;
	case PDTEqualNum_Em:
		if (i==0)
			cout<<"==";
		break;
	case PDTEqualBool_Em:
		if (i==0)
			cout<<"==";
		break;
	case PDTNotEqualNum_Em:
		if (i==0)
			cout<<"!=";
		break;
	case PDTNotEqualBool_Em:
		if (i==0)
			cout<<"!=";
		break;
	case PDTNeg_Em:
		break;
	case PDTNot_Em:
		break;
	case PDTListOfStatements_Em:
		;
		break;
	default:
		;
	}
	return true;

}
/*
  post is executed after traversing the children
*/
bool PDTDefaultVisitor::post(PDTNode * me){
	NodeTypeEnum type =me->getType();
	switch (type)
	{
/*	case (PDTNumVar_Em||PDTNumConstInt_Em||PDTNumConstDbl_Em||PDTBoolVar_Em||PDTBoolConst_Em):
		break;
		*/

	case PDTAdd_Em:
		cout<<")";
		break;
	case PDTSubt_Em:
		cout<<")";
		break;
	case PDTMult_Em:
		cout<<")";
		break;
	case PDTDiv_Em:
		cout<<")";
		break;
	case PDTMod_Em:
		cout<<")";
		break;
	case PDTAssign_Em:
		cout<<";\n";
		break;
	case PDTWhile_Em:
		cout<<"}\n";
		break;
	case PDTFunctionDec_Em:
		cout<<";\n}\n";
		break;
	case PDTIfElse_Em:
		cout<<"}\n";
		break;
	case PDTAnd_Em:
		cout<<")";
		break;
	case PDTOr_Em:
		cout<<")";
		break;
	case PDTLessThan_Em:
		cout<<")";
		break;
	case PDTGreaterThan_Em:
		cout<<")";
		break;
	case PDTLessThanEqual_Em:
		cout<<")";
		break;
	case PDTGreaterThanEqual_Em:
		cout<<")";
		break;
	case PDTEqualNum_Em:
		cout<<")";
		break;
	case PDTEqualBool_Em:
		cout<<")";
		break;
	case PDTNotEqualNum_Em:
		cout<<")";
		break;
	case PDTNotEqualBool_Em:
		cout<<")";
		break;
	case PDTNeg_Em:
		break;

	case PDTNot_Em:
		;
		break;
	
	case PDTListOfStatements_Em:
		;
		break;
	default:
		;
	}
	return true;
}
/*
utility function to convert an integer to a character
*/
char *inttochar(int i){
	char *temp=new char (100); //maybe increase then delete.
	sprintf(temp,"%d",i);
	return temp;
}
/*
utility function to convert a double to a character
*/
char *doubletochar(double i){
	char *temp=new char (100); //maybe increase then delete.
	sprintf(temp,"%f",i);
	return temp;
}
/*
utility function to convert a string to a character array
*/
char *  PDTYicesVisitor::stringToCharArray(string s){
	return (char*)s.c_str();
}

/*
utility function to convert a constant character array to a character array
*/
char * PDTYicesVisitor::constCharToChar(const char * cArray){
	return const_cast<char *> (cArray);
}
/*
function that takes a string containing the yices command, executes it, and returns the result
*/
int PDTYicesVisitor::writeToYices(string statement){
	char *temp=new char[statement.length()+1];
	strcpy(temp,statement.c_str());
	int i=yicesl_read(lctx,temp);
	if (i==1)
		cout<<statement<<endl;
		//cout<<yicesl_get_last_error_message()<<"\n";

	return i;
}
/*
function that takes a char array containing the yices command, executes it, and returns the result
*/
int PDTYicesVisitor::writeToYices( char * statement){

	int i=yicesl_read(lctx,statement);
	if (i==1)
		cout<<statement<<endl;
		//cout<<yicesl_get_last_error_message()<<"\n";

	return i;
}
/*
function that takes a constant char array containing the yices command, executes it, and returns the result
*/
int PDTYicesVisitor::writeToYices(const char * statement){
	char *temp=new char[strlen(statement)+1];
	strcpy(temp,statement);
	int i=yicesl_read(lctx,temp);
	if (i==1)
		cout<<statement<<endl;
		//cout<<yicesl_get_last_error_message()<<"\n";

	return i;
}


/*
constructor for the PDTYicesVisitor class that takes a PDTCodeGraph and does the initializations and executes
the first statements in yices
*/
PDTYicesVisitor::PDTYicesVisitor(PDTCodeGraph &CG){
	ctx=yices_mk_context();
	firstTime=true;
	assignTarget=false;
	ifCondition=false;
	lctx= yices_get_lite_context(ctx);
	writeToYices("(set-evidence! true)");
	writeToYices("(set-verbosity! 3)");
	writeToYices("(define-type _exp)");
        writeToYices("(define-type _i (-> int int))");
	writeToYices("(define-type _b (-> int bool))");
	writeToYices("(define _EC::(-> _exp int))");
	writeToYices("(define _ival::(-> _exp int))");
	writeToYices("(define _bval::(-> _exp bool))");
	writeToYices("(define e0::_exp)");
	writeToYices("(define e_end::_exp)");
	writeToYices("(assert (= (_EC e0) 0))");

	currentID=0;
	previousID=-1;
	currentAssertion="";

}
/*
prints the execution counter
*/
void PDTYicesVisitor::ECPrinter(){
	currentAssertion.append(" (_EC e").append(inttochar(previousID)).append(" ) ");


}
/*
appends one paranthesis to the current assertion statement
*/
void  PDTYicesVisitor::appendParan(){
	currentAssertion.append(")");
}

/*
updates previousID to currentID, increments currentID, and defines currentID in yices
*/
void PDTYicesVisitor::updateIDs(bool assertGreater){
	string statement="";
	previousID=currentID;
	currentID++;
	char input[100];
	sprintf(input,"(define e%d::_exp)",currentID);
	writeToYices(input);
/* assertGreater is false when we have an if statement where the assertion of greater than is done conditionally
i.e. depending on the if content
*/
	if (assertGreater){
		sprintf(input,"(assert+ (> (_EC e%d) (_EC e%d)))",currentID,previousID);
		writeToYices(input);
	}


}
/*
extracts the name from PDTNumVar, defines a variable in yices and defines a generic
variable (maybe this last step isn't needed)
*/
int  PDTYicesVisitor::declareNumVar(PDTNode * me){
	string varNameTemp=((PDTNumVar*)me)->getName();
	char * varName=stringToCharArray(varNameTemp);
	char * statement= new char[strlen(varName)+200]; //this can fail if the variable is too long
	sprintf(statement,"(define %s::_i)",varName);
	int i=writeToYices(statement);
	if (i!=0)
	{
		sprintf(statement,"(define %s_generic::_i)",varName);
		writeToYices(statement);
		sprintf(statement,"(assert+ (= %s_generic (lambda (i::int) (if (and (> i 0) (< i (_EC e_end))) (%s_generic (- i 1)) (%s_generic i)))))",varName,varName,varName);
		writeToYices(statement);
	}
	return i;
}
/*
extracts the name from booleans, defines a variable in yices
*/
int  PDTYicesVisitor::declareBoolVar(PDTNode * me){
	string statement="(define ";
	statement.append(((PDTNumVar*)me)->getName()).append("::(-> int bool))");

	return writeToYices(statement);

}

/*
This function is executed before children are traversed
*/
bool PDTYicesVisitor::pre(PDTNode * me){
	NodeTypeEnum type =me->getType();
//	if ( (type==PDTAnd_Em) || (type==PDTOr_Em) || (type==PDTEqualBool_Em) || (type==PDTNotEqualBool_Em) || (type==PDTEqualNum_Em)
//		|| (type==PDTNotEqualNum_Em) || (type==PDTGreaterThan_Em) || (type==PDTGreaterThanEqual_Em) || (type==PDTLessThan_Em)
//		|| (type==PDTLessThanEqual_Em_Em))


	string statement="";
	switch (type)
	{
	case PDTNumVar_Em:
		if (assignTarget)
			currentAssertion.append("(_ival e").append(inttochar(currentID)).append(") ");
		else
			currentAssertion.append("(").append(((PDTNumVar*)me)->getName());
		declareNumVar(me);
		break;

	case PDTNumConstInt_Em:
		currentAssertion.append(inttochar(((PDTNumConstInt *)me)->getValue()));
		break;
	case PDTNumConstDbl_Em:
		currentAssertion.append(doubletochar(((PDTNumConstDbl *)me)->getValue()));
		break;
	case PDTBoolVar_Em:
		if (assignTarget) //in case of boolean assignment or if condition
			currentAssertion.append("(_bval e").append(inttochar(currentID)).append(") ");
		else
			currentAssertion.append("(").append(((PDTBoolVar*)me)->getName());

		declareBoolVar(me);
		break;
	case PDTBoolConst_Em:
		if(((PDTBoolConst *)me)->getValue()==false)
			currentAssertion.append("false");
		else
			currentAssertion.append("true");
		break;
	case PDTAdd_Em:
		currentAssertion.append("(+ ");
		break;
	case PDTSubt_Em:
		currentAssertion.append("(- ");
		break;
	case PDTMult_Em:
		currentAssertion.append("(* ");
		break;
	case PDTDiv_Em:
		currentAssertion.append("(/ ");
		break;
	case PDTMod_Em:
		currentAssertion.append("(mod ");
		break;
	case PDTAssign_Em://////////
		updateIDs(true);
		assignTarget=true;
		currentAssertion="(assert+ (= "	;
		break;
	case PDTWhile_Em://///////////
		cout<<"while( ";
		break;
	case PDTIfElse_Em://///////		
		updateIDs(true);
		ifCondition=true;
		ifHelper.push(currentID);//push the if condition expression id
		currentAssertion="(assert+ (= (_bval e"	;
		currentAssertion.append(inttochar(currentID)).append(") ");
		break;
	case PDTAnd_Em:		
		currentAssertion.append("(and ");
		break;
	case PDTOr_Em:
		currentAssertion.append("(or ");
		break;
	case PDTLessThan_Em:
		currentAssertion.append("(< ");
		break;
	case PDTGreaterThan_Em:
		currentAssertion.append("(> ");
		break;
	case PDTLessThanEqual_Em:
		currentAssertion.append("(<= ");
		break;
	case PDTGreaterThanEqual_Em:
		currentAssertion.append("(>= ");
		break;
	case PDTEqualNum_Em:
		currentAssertion.append("(= ");
		break;
	case PDTEqualBool_Em:
		currentAssertion.append("(= ");
		break;
	case PDTNotEqualNum_Em:
		currentAssertion.append("(/= ");
		break;
	case PDTNotEqualBool_Em:
		currentAssertion.append("(/= ");
		break;
	case PDTNeg_Em://///////////
		cout<<"-";
		break;
	case PDTNot_Em:///////
		break;
	case PDTListOfStatements_Em://///////////
		;
		break;
	default:
		;
	}
	return true;
}

/*
This function is executed between each two children traversal
*/
bool PDTYicesVisitor::in(PDTNode * me, PDTNode* child, unsigned int i){
	NodeTypeEnum type =me->getType();
	char tempIf[200];
	int ifCond;

	switch (type)
	{
/*	case (PDTNumVar_Em||PDTNumConstInt_Em||PDTNumConstDbl_Em||PDTBoolVar_Em||PDTBoolConst_Em):
		break;
*/
	case PDTNumConstInt_Em:	
		break;
	case PDTNumVar_Em:
		break;
	case PDTAdd_Em:
		break;
	case PDTSubt_Em:

		break;
	case PDTMult_Em:

		break;
	case PDTDiv_Em:

		break;
	case PDTMod_Em:

		break;
	case PDTAssign_Em:
		//(yicesHelper[me->getId()]).args[i]=(yicesHelper[child->getId()]).expr;
		if (i==0)
			//currentAssertion.append(" (_EC e").append(inttochar(currentID)).append(" ))");
			assignTarget=false;
		break;
	case PDTWhile_Em://///////////
		if (i==0)
			cout<<") {\n";
		break;
	case PDTIfElse_Em:////
		if (i==0)
		{
			ifCondition=false;
			currentAssertion.append("))");
		//	cout<<currentAssertion<<endl;
			writeToYices(currentAssertion);
			updateIDs(false);
			sprintf(tempIf,"(assert+ (= true (if (_bval e%d) (= (_EC e%d) (_EC e%d)) (> (_EC e%d) (_EC e_end) ) ) ))",
				previousID,currentID,previousID,currentID);
			writeToYices(tempIf);
		}
		else if (i==1)
		{
			updateIDs(false);
			ifCond=ifHelper.top();
			sprintf(tempIf,"(assert+ (= true (if (not (_bval e%d)) (= (_EC e%d) (_EC e%d)) (> (_EC e%d) (_EC e_end) ) ) ))",
				ifCond,currentID,ifCond,currentID);
			writeToYices(tempIf);
			ifHelper.push(previousID);//push the last statement id in if block
		}

		break;
	case PDTAnd_Em:

		break;
	case PDTOr_Em:

		break;
	case PDTLessThan_Em:

		break;
	case PDTGreaterThan_Em:

		break;
	case PDTLessThanEqual_Em:

		break;
	case PDTGreaterThanEqual_Em:

		break;
	case PDTEqualNum_Em:

		break;
	case PDTEqualBool_Em:

		break;
	case PDTNotEqualNum_Em:

		break;
	case PDTNotEqualBool_Em:

		break;
	case PDTNeg_Em://///////////
		break;
	case PDTNot_Em:
	//	(yicesHelper[me->getId()]).args[i]=(yicesHelper[child->getId()]).expr;
		break;
	case PDTListOfStatements_Em://///////////
		;
		break;	

	case PDTProp_Em:
	//	(yicesHelper[me->getId()]).expr=(yicesHelper[child->getId()]).expr;
		break;

	default:
		;
	}
	return true;

}
/*
This function is executed after traversing the children
*/
bool PDTYicesVisitor::post(PDTNode * me){
	NodeTypeEnum type =me->getType();
	char tempIf[200];
	int lastInIf,ifCond;
	switch (type)
	{
/*	case (PDTNumVar_Em||PDTNumConstInt_Em||PDTNumConstDbl_Em||PDTBoolVar_Em||PDTBoolConst_Em):
		break;
		*/
	case (PDTNumVar_Em):
		if (!assignTarget)
		{
			ECPrinter();
			appendParan();
		}
		break;
	case (PDTBoolVar_Em):
		if (!assignTarget)
		{
			ECPrinter();
			appendParan();
		}
		break;
	case PDTNumConstInt_Em:
		break;
	case PDTAdd_Em:
		appendParan();
		break;
	case PDTSubt_Em:
		appendParan();
		break;
	case PDTMult_Em:
		appendParan();
		break;
	case PDTDiv_Em:///////////
		appendParan();
		break;
	case PDTMod_Em://///////
		appendParan();
	case PDTAssign_Em:///////
		appendParan();appendParan();
		firstTime=false;
		writeToYices(currentAssertion);
		break;
	case PDTWhile_Em:////////
		//cout<<"}\n";
		break;
	case PDTIfElse_Em://////
		//appendParan();
	//	cout<<")";
		updateIDs(false);
		lastInIf=ifHelper.top();
		ifHelper.pop();
		ifCond=ifHelper.top();
		ifHelper.pop();
		sprintf(tempIf,"(assert+ (= (_EC e%d) (if (_bval e%d) (_EC e%d) (_EC e%d) )))",
			currentID,ifCond,lastInIf,previousID);

		writeToYices(tempIf);
		break;
	case PDTAnd_Em:
		appendParan();
		break;
	case PDTOr_Em:
	//	(yicesHelper[me->getId()]).expr=yices_mk_or(ctx,(yicesHelper[me->getId()]).args,2);
		break;
	case PDTLessThan_Em:
		appendParan();
		break;
	case PDTGreaterThan_Em:
		appendParan();
		break;
	case PDTLessThanEqual_Em:
		appendParan();
		break;
	case PDTGreaterThanEqual_Em:
		appendParan();
		break;
	case PDTEqualNum_Em:
		appendParan();
		break;
	case PDTEqualBool_Em:
		appendParan();
		break;
	case PDTNotEqualNum_Em:
		appendParan();
		break;
	case PDTNotEqualBool_Em:
		appendParan();
		break;
	case PDTNeg_Em://///////
		break;

	case PDTNot_Em:
	//	(yicesHelper[me->getId()]).expr=yices_mk_not(ctx,(yicesHelper[me->getId()]).args[0]);
		break;

	case PDTListOfStatements_Em://///////
		break;
	case PDTProp_Em:
	//	yices_assert(ctx, (yicesHelper[me->getId()]).expr);
	//	yices_pp_expr((yicesHelper[me->getId()]).expr);
		break;
	default:
		;
	}
	return true;
}
